nat-deq  EqDecider() 

latex

Definitions	t  T, EqDecider(T), nat-deq, x:A. B(x), P  Q, prop{i:l}, P  Q, P  Q, P  Q,
Lemmas	eq int wf, nat wf, iff wf, assert wf